#547 Decouple Solver Component into Standalone Crate #25
Conversation
momvart
left a comment
momvart
left a comment
There was a problem hiding this comment.
Thanks for the effort.
An important missing piece:
As I mentioned before, except sanity checking, we will negate some constraints to derive a new input. Currently, we don't have any mechanism for that. Although implementing it will be done by supporting a view on the query, for now we can have an option to negate the last constraint as a minimum.
Beside that, things look fine for now. I'll rebase to your branch and use your binary for actual solving.
| match output.result.as_str() { | ||
| "sat" => println!( | ||
| "✓ SAT - Solution found and written to {}", | ||
| args.output.display() | ||
| ), | ||
| "unsat" => println!("✗ UNSAT - No solution exists"), | ||
| "unknown" => println!("? UNKNOWN - Could not determine satisfiability"), | ||
| _ => unreachable!("Unexpected result: {}", output.result), | ||
| } |
There was a problem hiding this comment.
Use macros in common:logging for logging.
|
|
||
| let constraint_value = json_value | ||
| .as_object_mut() | ||
| .and_then(|obj| obj.remove("constraint")) |
There was a problem hiding this comment.
Make sure you use consts for these stuff.
| /// Input format for JSONL constraint files | ||
| #[derive(Debug, Serialize, Deserialize)] | ||
| pub struct ConstraintEntry { | ||
| pub step: StepInfo, |
|
|
||
| // Serialization support for binary interface | ||
| #[cfg(feature = "serde")] | ||
| pub mod format { |
There was a problem hiding this comment.
As this format only concerns the binary, I'd like it out of the library but in the binary's module
| } | ||
|
|
||
| #[test] | ||
| fn test_constraint_kind_operations() { |
There was a problem hiding this comment.
Thanks for writing the tests. I see some of them are focused on common's data structures. Why not moving them there next to their definitions?
momvart
changed the title
This PR extracts the SMT solving functionality from the codebase into a standalone
leafsolvercrate. The new crate provides both a library interface and a CLI binary